T:Type, ll1, ll2:(T List) List. ll1  ll2  concat(ll1)  concat(ll2) 

latex

Definitions	S  T, Top, l1  l2, P  Q, x:A. B(x), Prop, as @ bs, concat(ll), x:A. B(x), t  T
Lemmas	concat wf, append wf, top wf, concat append